1. Field of the Invention
The invention relates to a process for managing, a method of verifying and a method of transforming a downloaded program fragment and the corresponding systems, more particularly intended for embedded data-processing systems with limited memory and of computing power resources.
2. Prior Art
In a general way, by reference to FIG. 1a, it is reiterated that embedded data-processing systems 10 include a microprocessor 11; a computer readable storage medium, including, but not limited to: a permanent memory, such as a non-writable memory 12 containing the code of the executable program, and a rewritable, nonvolatile, permanent memory 13 of EEPROM type containing the data stored in the system, a volatile, random-access memory 14 in which the program stores its intermediate results while it is executing; and input/output devices 15 allowing the system to interact with its environment. When the embedded data-processing system consists of a microprocessor card, of the bank-card type, the input/output device 15 consists of a serial link allowing the card to communicate with a terminal, such as a card-reader terminal.
In conventional embedded data-processing systems, the code of the program executed by the system is fixed during construction of the system, or, at the latest, when the latter is customized before delivery to the final user.
More sophisticated embedded data-processing systems have, however, been implemented, these systems being reprogrammable, such as microprocessor cards of the JAVACARD type, for example. Compared to the earlier types, these reprogrammable systems add the possibility of enhancing the program after the system has been put into service, via an operation of downloading program fragments. These program fragments, commonly known as “applets”, will be referred to as applets or program fragments indiscriminately in the present description. For a more detailed description of JAVACARD systems, reference could usefully be made to the documentation published by the company SUN MICROSYSTEMS INC., and in particular to the electronically available documentation, JAVACARD technology chapter, on the World Wide Web at site http://java.sun.com/products/javacard/index.html, available since June 1999.
FIG. 1b illustrates the architecture of such a reprogrammable embedded data-processing system. This architecture is similar to that of a conventional embedded system, apart from the fact that the reprogrammable embedded system can in addition receive applets via one of its input/output devices, then store them in its permanent memory 13 from which they can then be executed complementing the main program.
For reasons of portability between different embedded data-processing systems, applets take the form of code for a standard virtual machine. This code is not directly executable by the microprocessor 11, but it has to be interpreted in software terms by a virtual machine 16, which consists of a program resident in a non-writable permanent memory 12. In the above-mentioned example of JAVACARD cards, the virtual machine used is a subset of the JAVA virtual machine. For a description of the specifications relating to the JAVA virtual machine and of the virtual machine used, reference could usefully be made to the work published by Tim LINDHOLM and Frank YELLIN, entitled “The Java Virtual Machine Specification”, Addison-Wesley 1996, and to the documentation published by the company SUN MICROSYSTEMS INC. “JAVACARD 2.1 Virtual Machine Specification”, documentation available electronically on the World Wide Web at site http://java.sun.com/products/javacard/JCVMSpec.pdf, since March 1999.
The operation of downloading applets onto an embedded data-processing system in service poses considerable security problems. An applet which is unintentionally, or even deliberately, badly written may incorrectly modify data present on the system, prevent the main program from being executed correctly or at the right time, or even modify other applets downloaded previously, making them unusable or harmful.
An applet written by a computer hacker may also divulge confidential information stored in the system, information such as the access code in the case of a bank card, for example.
At the present time, three solutions have been proposed with a view to remedying the problem of applet security.
A first solution consists in using cryptographic signatures in order to accept only applets originating from trusted organizations or persons.
In the abovementioned example of a bank card, only the applets bearing the cryptographic signature of the bank having issued the card are accepted and executed by the card, any other unsigned applet being rejected in the course of the downloading operation. An ill-intentioned user of the card, not having available encryption keys from the bank, will therefore be unable to execute an unsigned and dangerous applet on the card.
This first solution is well suited to the case where all the applets originate from the same single source, the bank in the abovementioned example. This solution is difficult to apply in the case where the applets originate from several sources, such as, in the example of a bank card, the card manufacturer, the bank, the organizations managing bank card services, the large commercial distribution organizations offering customers loyalty programs and legitimately offering to download specific applets onto the card. The sharing and the holding among these various economic participants of the encryption keys necessary for the electronic signature of the applets pose major technical, economic and legal problems.
A second solution consists in carrying out dynamic access and typing checks while executing the applets.
In this solution, the virtual machine carries out a certain number of checks, while executing the applets, such as:                memory access check: upon each read or write in a memory area, the virtual machine verifies the right of access by the applet to the corresponding data;        dynamic verification of the data types: upon each instruction from the applet, the virtual machine verifies that the constraints on the data types are satisfied. By way of example, the virtual machine may apply special processing to data such as valid memory addresses, and prevent the applet generating invalid memory addresses by way of integer/address conversions or arithmetic operations on the addresses;        detection of stack overflows and of illegal accesses to the execution stack of the virtual machine, which, under certain conditions, are likely to disturb the operation thereof, to the point of circumventing the preceding check mechanisms.        
This second solution allows execution of a wide range of applets under satisfactory security conditions. However, it presents the drawback of a considerable slowing of the execution, caused by the range of dynamic verifications. In order to obtain a reduction in this slowing effect, some of these verifications can be managed by the microprocessor itself, at the cost, however, of an increase in the complexity thereof and thus of the cost price of the embedded system. Such verifications furthermore increase the random-access and permanent memory requirements of the system, because, of the additional type information which must be associated with the data handled.
A third solution consists in carrying out a static verification of the code of the applet during the downloading.
In this solution, this static verification simulates the execution of the applet at the level of the data types and establishes, once and for all, that the code of the applet complies with the rule of data types and of access control imposed by the virtual machine and does not cause a stack overflow. If this static verification is successful, the applet can then be executed without it being necessary dynamically to verify that this rule is complied with. In the event that the static verification process fails, the embedded system rejects the “applet” and does not allow its subsequent execution. For a more detailed description of the abovementioned third solution, reference could usefully be made to the work published by Tim LINDHOLM and Frank YELLIN quoted above, to the article published by James A. GOSLING entitled “Java Intermediate Byte Codes”, proceedings of the ACM SIGPLAN, Workshop on Intermediate Representations (IR'95), pages 111-118, January 1995, and to the U.S. Pat. No. 5,748,964 granted on May 5, 1998.
Compared with the second solution, the third solution presents the advantage of a much more rapid execution of the applets, since the virtual machine does not carry out any verification during execution.
The third solution, however, presents the drawback of a process of static verification of the code which is complex and expensive, both in terms of size of code necessary to conduct this process and in terms of size of random-access memory necessary to contain the intermediate results of the verification, and in terms of computation time. By way of illustrative example, the code verification incorporated in the JAVA JDK system marketed by SUN MICROSYSTEMS represents about 50 kbytes of machine code, and its consumption in terms of random-access memory is proportional to (Tp+Tr)×Nb, where Tp designates the maximum stack space, Tr designates the maximum number of registers and Nb designates the maximum number of branch targets used by a subroutine, also commonly called method, of the applet. These memory requirements greatly exceed the capacities of the resources of most present-day embedded data-processing systems, especially of commercially available microprocessor cards.
Several variants of the third solution have been proposed, in which the publisher of the applet sends to the verifier, in addition to the code of the applet, a certain amount of specific supplementary information such as precalculated data types or preestablished proof of correct data typing. For a more detailed description of the corresponding procedures, reference could usefully be made to the articles published by Eva ROSE and Kristoffer HØGSBRO ROSE, “Lightweight Bytecode Verification”, proceedings of the Workshop on Formal Underspinning of JAVA, October 1998, and by George C. NECULA, “Proof-Carrying Code”, Proceedings of the 24th ACM Symposium on Principles of Programming Languages, pages 106-119, respectively.
This supplementary information makes it possible to verify the code more rapidly and slightly to reduce the size of the verification program code but does not make it possible, however, to reduce the requirements for random-access memory, and even increases them, very substantially, in the case of the correct-data-typing preestablished-proof information.